#parser.py
import parse_utils, re

#regexes
matchNegation = re.compile(r"^not\s*-$|^-$|^not\s*$")
matchNegationB = re.compile(r"^,\s*not\s*-$|^,\s*-$|^,\s*not\s*$")
isVar = re.compile(r"^[A-Z]\w*")

#Used data structures
#Atom:       (3, predicate_name, string, [terms])
#Aggregate:  (2, function, vars, rule, ops)
#Quantifier: (1, function, vars, rule, rule)
#Unknown:    (0, string)

#Rule: ( type,
#	[Atom|Aggregate|Quantifier|Unknown],
#	[Atom|Aggregate|Quantifier|Unknown] )
#where type: 0->normal, 1->cr-rule

#parsed structures: (type, id, string)

#allowed aggregates functions
aggr_funcs = ['#count', '#sum', '#times', '#max', '#min']

#returns a parsed, syntactically correct Atom
#ratom is of the form (3, pred, str)
def parseAtom(ratom):
	parts = parse_utils.getTerms(ratom[2])
	return (3, ratom[1].strip(), ratom[2], parts)

#parses a comma separated list of literals or eliterals
#returns a list of Atoms with strings representing the (e)literal or (3,str,None,[])
def parseAtomList(atomlist):
	parts = parse_utils.getParams(atomlist,True)
	atoms = []
	prefix = ''
	hassep = True
	#check first unkown
	if parts[0][0] == 0:
		if matchNegation.match(parts[0][2].strip()):
			prefix = parts[0][2]
			i = 1
		else:
			raise Exception('Syntax error')
	else:
		i = 0
	#check if no garbage at end
	if parts[-1][0] == 0:
		raise Exception('Syntax error')
	#check parts
	while i < len(parts):
		part = parts[i]
		str = part[2].strip()
		if part[0] == 0:
			hassep = True
			#check if comma or negation
			if matchNegationB.match(str):
				prefix = str[1:]
			elif str == ',':
				i += 1
				continue
			else:
				raise Exception('Syntax error')
		#else, atom already
		elif hassep:
			if len(prefix) > 0:
				#add prefix to atom string
				parsed = parseAtom(part)
				if 'not' in prefix:
					prefix = prefix+' '
				nstr = prefix+parsed[2]
				prefix = ''
				atoms.append((3,parsed[1],nstr,parsed[3]))
			else:
				atoms.append(parseAtom(part))
			hassep = False
		#no separator
		else:
			raise Exception('Syntax error')
		i += 1
	return atoms


#returns a parsed, syntactically correct Aggregate
#ragg is of the form (2, #func, str)
#note: str='#func(...) op word'
def parseAggregate(ragg):
	#check function name
	func = ragg[1].strip()
	if not func in aggr_funcs:
		raise Exception('Syntax error')
	#split into parts: rvars, rliterals, ops
	(ignore,sep,rest) = ragg[2].partition('(')
	(rvars,sep,rest) = rest.partition(':')
	if len(sep) == 0:
		raise Exception('Syntax error')
	(rliterals,sep,ops) = rest.rpartition(')')
	#trick: use getPredicates to get variables
	(ignore,vars) = parse_utils.getPredicate('p('+rvars+')')
	#check if vars are vars
	for var in vars:
		if not isVar.match(var):
			raise Exception('Syntax error')
	#get literals
	literals = parseAtomList(rliterals.strip())
	return (2, func, vars, literals, ops)

#returns a parsed, syntactically correct Aggregate
#rquant is of the form (2, #func, str)
def parseQuantifier(rquant,label):
	#check function name
	func = rquant[1].strip()
	if func != label:
		raise Exception('Syntax error')
	#split into parts: rvars, rliterals, ops
	(ignore,sep,rest) = rquant[2].partition('[')
	(rvars,sep,rest) = rest.partition(':')
	if len(sep) == 0:
		raise Exception('Syntax error')
	(rdomain,sep,rrange) = rest.rpartition(']')
	#trick: use getPredicates to get variables
	(ignore,vars) = parse_utils.getPredicate('p('+rvars+')')
	#check if vars are vars
	for var in vars:
		if not isVar.match(var):
			raise Exception('Syntax error')
	#get domain
	rdomain = rdomain.strip()
	domain = parseAtomList(rdomain)
	#range
	rrange = rrange[rrange.find('(')+1:rrange.rfind(')')].strip()
	range = parseAtomList(rrange)
	return (1, func, vars, domain, range)

#input: a SPARC rule as a string
#returns a Rule as defined in the header of the document
def parseRule(rule):
	head = []
	body = []
	rbody = ''
	rhead = ''
	#get type: 0-> normal, 1->cr-rule
	type = 0
	ifpos = rule.find(':+')
	if ifpos == -1:
		ifpos = rule.find(':-')
	else:
		#cr
		type = 1
	if ifpos == -1:
		#we have a fact
		rhead = rule
	else:
		#split rule
		rhead = rule[:ifpos].strip()
		rbody = rule[ifpos+2:].strip()
	#parse head
	if len(rhead) > 0:
		parts = parse_utils.getParams(rhead,False)
		for part in parts:
			if part[0] == 0:
				#add unknown
				head.append((0,part[2]))
			elif part[0] == 1:
				#add exists
				head.append(parseQuantifier(part,'#exists'))
			elif part[0] == 3:
				head.append(parseAtom(part))
			else:
				raise Exception('Syntax error')
	#parse body
	if len(rbody) > 0:
		parts = parse_utils.getParams(rbody,False)
		for part in parts:
			if part[0] == 0:
				#add unknown
				body.append((0,part[2]))
			elif part[0] == 1:
				#add exists
				body.append(parseQuantifier(part,'#forall'))
			elif part[0] == 2:
				#add aggregate
				body.append(parseAggregate(part))
			elif part[0] == 3:
				body.append(parseAtom(part))
			else:
				raise Exception('Syntax error')
	return (type,head,body)

def parse(rule):
	(type,head,body) = parseRule(rule)
	lbls = ['normal rule', 'cr-rule']
	print lbls[type]
	print 'head:'
	for comp in head:
		print comp
	print 'body:'
	for comp in body:
		print comp